\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{BoolExp} : \coqdockw{Type} := \coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_lit} : \coqdocvar{Bool}     \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_id}  : \coqdocvar{Id}       \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_eq}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_lt}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_le}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_gt}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_gtb} : \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_eqb} : \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_ge}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_not} : \coqdocvar{BoolExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_and} : \coqdocvar{BoolExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_exp\_or}  : \coqdocvar{BoolExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}  \ensuremath{\rightarrow} \coqdocvar{BoolExp}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
